open Syntax
open Hashtbl
open BlockPopulation
open Binding




module Proof : sig
	type proof =  
		| Partial of ty * proof option
		| ProgNode of ty 
		| ForAllElim of proof * ty
		| ImplyElim of proof * proof
		
	val is_complete : proof->bool
	val is_equiv : context->proof->proof->bool
end 


open Proof
module ProoProg  : sig
	type program =  In of int | TypeFunc of program * ty | ObjFunc of program * program
	val string_of_program : GenePool.gene_pool -> (proof * program) -> string
end 


open ProoProg
val check_tree : context -> proof -> ty
val exists : context -> proof list -> proof -> bool 

val width : context->ty->ty->int

val string_of_proof : ?output:string -> ?separator:string -> ?line_break:string 
	-> context -> proof -> string
val dotGraphs : context -> proof list -> string
	
val progs_of_proof : ?debug:bool->GenePool.gene_pool->proof->program list	
val term_of_program : ?debug:bool->GenePool.gene_pool->proof->program->term
val prog_num : GenePool.gene_pool->proof list->int
(*val make_proofs : proof list->int -> gene_pool -> ty -> proof list


*)